Example Section 4.2 in [Duran, Lucas, Marché, Meseguer & Urbain - PEPM'04]

Summary: ExSec4_2_DLMMU04

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'
• Positive results:
  1. CSRPO
  2. Zantema's transformation
  3. Ferreira and Ribeiro's transformation

ExSec4_2_DLMMU04 in TPDB format ( ExSec4_2_DLMMU04.trs):

(VAR N XS YS X ZS)
(STRATEGY CONTEXTSENSITIVE 
  (natsFrom 1)
  (cons 1)
  (s 1)
  (fst 1)
  (pair 1 2)
  (snd 1)
  (splitAt 1 2)
  (0)
  (nil)
  (u 1)
  (head 1)
  (tail 1)
  (sel 1 2)
  (afterNth 1 2)
  (take 1 2)
)
(RULES 
natsFrom(N) -> cons(N,natsFrom(s(N)))
fst(pair(XS,YS)) -> XS
snd(pair(XS,YS)) -> YS
splitAt(0,XS) -> pair(nil,XS)
splitAt(s(N),cons(X,XS)) -> u(splitAt(N,XS),N,X,XS)
u(pair(YS,ZS),N,X,XS) -> pair(cons(X,YS),ZS)
head(cons(N,XS)) -> N
tail(cons(N,XS)) -> XS
sel(N,XS) -> head(afterNth(N,XS))
take(N,XS) -> fst(splitAt(N,XS))
afterNth(N,XS) -> snd(splitAt(N,XS))
)

The CS-TRS in OBJ format (file ExSec4_2_DLMMU04.obj):

obj ExSec4_2_DLMMU04 is
  sort S .
  op natsFrom : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op fst : S -> S .
  op pair : S S -> S .
  op snd : S -> S .
  op splitAt : S S -> S .
  op 0 : -> S .
  op nil : -> S .
  op u : S S S S -> S [strat (1 0)] .
  op head : S -> S .
  op tail : S -> S .
  op sel : S S -> S .
  op afterNth : S S -> S .
  op take : S S -> S .
  vars N XS YS X ZS : S .
  eq natsFrom(N) = cons(N,natsFrom(s(N))) .
  eq fst(pair(XS,YS)) = XS .
  eq snd(pair(XS,YS)) = YS .
  eq splitAt(0,XS) = pair(nil,XS) .
  eq splitAt(s(N),cons(X,XS)) = u(splitAt(N,XS),N,X,XS) .
  eq u(pair(YS,ZS),N,X,XS) = pair(cons(X,YS),ZS) .
  eq head(cons(N,XS)) = N .
  eq tail(cons(N,XS)) = XS .
  eq sel(N,XS) = head(afterNth(N,XS)) .
  eq take(N,XS) = fst(splitAt(N,XS)) .
  eq afterNth(N,XS) = snd(splitAt(N,XS)) .
endo

Negative results

1. The µ-termination of ExSec4_2_DLMMU04 cannot be proved by using Lucas' transformation. The TRS ExSec4_2_DLMMU04_L:

   	natsFrom(N) -> cons(N)
   	fst(pair(XS,YS)) -> XS
   	snd(pair(XS,YS)) -> YS
   	splitAt(0,XS) -> pair(nil,XS)
   	splitAt(s(N),cons(X)) -> u(splitAt(N,XS))
   	u(pair(YS,ZS)) -> pair(cons(X),ZS)
   	head(cons(N)) -> N
   	tail(cons(N)) -> XS
   	sel(N,XS) -> head(afterNth(N,XS))
   	take(N,XS) -> fst(splitAt(N,XS))
   	afterNth(N,XS) -> snd(splitAt(N,XS))
   
   

   contains extra variables.
   

Positive results

1. The µ-termination of ExSec4_2_DLMMU04 can be proved by using CSRPO MuTerm
2. The µ-termination of ExSec4_2_DLMMU04 can be proved by using Zantema' transformation. The TRS ExSec4_2_DLMMU04_Z:

   	natsFrom(N) -> cons(N,n__natsFrom(s(N)))
   	fst(pair(XS,YS)) -> XS
   	snd(pair(XS,YS)) -> YS
   	splitAt(0,XS) -> pair(nil,XS)
   	splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS))
   	u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS)
   	head(cons(N,XS)) -> N
   	tail(cons(N,XS)) -> activate(XS)
   	sel(N,XS) -> head(afterNth(N,XS))
   	take(N,XS) -> fst(splitAt(N,XS))
   	afterNth(N,XS) -> snd(splitAt(N,XS))
   	natsFrom(X) -> n__natsFrom(X)
   	activate(n__natsFrom(X)) -> natsFrom(X)
   	activate(X) -> X
   				

   can be proved terminating by AProVE
   
3. The µ-termination of Ex5_DLMMU04 can be proved by using Ferreira and Ribeiro's transformation' . The TRS ExSec4_2_DLMMU04_FR:

   				
   	natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
   	fst(pair(XS,YS)) -> XS
   	snd(pair(XS,YS)) -> YS
   	splitAt(0,XS) -> pair(nil,XS)
   	splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS))
   	u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS)
   	head(cons(N,XS)) -> N
   	tail(cons(N,XS)) -> activate(XS)
   	sel(N,XS) -> head(afterNth(N,XS))
   	take(N,XS) -> fst(splitAt(N,XS))
   	afterNth(N,XS) -> snd(splitAt(N,XS))
   	natsFrom(X) -> n__natsFrom(X)
   	s(X) -> n__s(X)
   	activate(n__natsFrom(X)) -> natsFrom(activate(X))
   	activate(n__s(X)) -> s(activate(X))
   	activate(X) -> X
   
   				

   can be proved terminating by AProVE